% RA: Relación 02
% OTTER: sumador.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% Diseñar un circuito lógico que implemente un sumador lógico de tres bits con
% componentes AND, OR y, como mucho, una única componente NOT.
%
%  Sumador de tres bits     Componente AND   Componente OR    Componente NOT
%
%     i1 i2 i3 | o1 o2        i1 i2 | o1       i1 i2 | o1        i1 | o1
%    ------------------      ------------     ------------      ---------
%     0  0  0  |  0  0        0  0  |  0       0  0  |  0        0  |  1
%     0  0  1  |  0  1        0  1  |  0       0  1  |  0        1  |  0
%     0  1  0  |  0  1        1  0  |  0       1  0  |  0
%     0  1  1  |  1  0        1  1  |  1       1  1  |  1
%     1  0  0  |  0  1
%     1  0  1  |  1  0
%     1  1  0  |  1  0
%     1  1  1  |  1  1

% Utilizar OTTER para encontrar una solución al problema.

%==============================================================================
% Formalización
%==============================================================================

set(hyper_res).
make_evaluable(_+_,$SUM(_,_)).
make_evaluable(_<=_,$LE(_,_)).

% Esta primera solución construye de forma explícita el circuito y no sería
% posible abordarla si no conociesemos la forma de hacerlo. 

%formula_list(sos).
% all x1 x2 x3
%  (salida(x1,x2,x3) -> salida(or(or(and(x1,x3),and(x1,x2)),and(x2,x3))),
%                              or(and(and(x1,x2),x3),not(or(or(and(x1,x2),and(x1,x3)),and(x2,x3))))).
%
%  salida(1,0,1).
%  -salida(1,0).
%end_of_list.

%list(demodulators).
% and(x,0) = 0.
% and(x,1) = x.
% or(x,0) = x.
% or(x,1) = 1.
% not(0) = 1.
% not(1) = 0.
%end_of_list.

formula_list(sos).
 all x1 x2 x3 x4 x5 x6 x7 x8 y1 y2 y3 y4 y5 y6 y7 y8 nx ny wx wy
  (salida(nx,x1,x2,x3,x4,x5,x6,x7,x8,$IGNORE(wx)) & salida(ny,y1,y2,y3,y4,y5,y6,y7,y8,$IGNORE(wy)) & nx+ny <= 1 ->
   salida(nx+ny,
          and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4),
          and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),$IGNORE([and,wx,wy]))).

 all x1 x2 x3 x4 x5 x6 x7 x8 y1 y2 y3 y4 y5 y6 y7 y8 nx ny wx wy
  (salida(nx,x1,x2,x3,x4,x5,x6,x7,x8,$IGNORE(wx)) & salida(ny,y1,y2,y3,y4,y5,y6,y7,y8,$IGNORE(wy)) & nx+ny <= 1 ->
   salida(nx+ny,
          or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4),
          or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),$IGNORE([or,wx,wy]))).

 all x1 x2 x3 x4 x5 x6 x7 x8 wx
  (salida(0,x1,x2,x3,x4,x5,x6,x7,x8,$IGNORE(wx)) ->
   salida(1,not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),not(x8),$IGNORE([not,wx]))).

 salida(0,0,0,0,0,1,1,1,1,$IGNORE([i1])).
 salida(0,0,0,1,1,0,0,1,1,$IGNORE([i2])).
 salida(0,0,1,0,1,0,1,0,1,$IGNORE([i3])).

 -(exists n1 n2 w1 w2 (salida(n1,0,0,0,1,0,1,1,1,$IGNORE(w1)) & salida(n2,0,1,1,0,1,0,0,1,$IGNORE(w2)) & n1+n2 <= 1)).
end_of_list.

list(demodulators).
 and(x,0) = 0.
 and(x,1) = x.
 or(x,1) = 1.
 or(x,0) = x.
 not(0) = 1.
 not(1) = 0.
end_of_list.

%==============================================================================

